Theory Infinite
theory Infinite
imports Main
begin
class infinite =
assumes infinite_UNIV: "infinite (UNIV :: 'a set)"
begin
lemma arb_element: "finite Y â¹ âx :: 'a. x â Y"
using ex_new_if_finite infinite_UNIV
by blast
lemma arb_finite_subset: "finite Y â¹ âX :: 'a set. Y â© X = {} â§ finite X â§ n ⤠card X"
proof -
assume fin: "finite Y"
then obtain X where "X â UNIV - Y" "finite X" "n ⤠card X"
using infinite_UNIV
by (metis Compl_eq_Diff_UNIV finite_compl infinite_arbitrarily_large order_refl)
then show ?thesis
by auto
qed
lemma arb_countable_map: "finite Y â¹ âf :: (nat â 'a). inj f â§ range f â UNIV - Y"
using infinite_UNIV
by (auto simp: infinite_countable_subset)
end
instance nat :: infinite
by standard auto
end
lass="head">
Theory FO
theory FO
imports Main
begin
abbreviation "sorted_distinct xs â¡ sorted xs â§ distinct xs"